M1, M2:MsgA. M1  M2  (a:Id, s:M2.state, v:M2.da(locl(a)). M2.pre(a,s,v)  M1.pre(a,s,v)) 

latex

Definitions	M.pre(a,s,v), M.da(a), M.state, M1  M2, MsgA, Valtype(da;k), P & Q, z != f(x)  P(a;z), x  dom(f), IdDeq, f(x), a:A fp B(a), State(ds), f(x)?z, x. t(x), KindDeq, locl(a), Top, Prop, IdLnk, Id, Knd, f  g, t  T, x:A. B(x), b, A & B, P  Q
Lemmas	top wf, locl wf, Kind-deq wf, Knd wf, fpf-cap wf, ma-state wf, Id wf, fpf-trivial-subtype-top, fpf-ap wf, id-deq wf, fpf-dom wf, assert wf, ma-da wf, ma-st wf, ma-sub wf, msga wf